COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	∂10-Jan-81  0110	NEUMANN at SRI-KL 	[Neumann: VERkshop II]    
C00059 ENDMK
C⊗;
∂10-Jan-81  0110	NEUMANN at SRI-KL 	[Neumann: VERkshop II]    
Date: 10 Jan 1981 0107-PST
From: NEUMANN at SRI-KL
Subject: [Neumann: VERkshop II]
To: JMC at SU-AI

John, I sent the first round of queries out to last year's list of
attendees, but want also to ask whether you are interested.  The results
from last year were mostly contained in the SOFTWARE ENGINEERING NOTES
July 1980 issue (ACM SIGSOFT).  I don't think you have been particularly
concerned with the security community (which is the origin of Walker's
interest in verification), but you certainly have had a long-standing
interest in verification.  HAPPY NEW YEAR in any event!  Best regards, Peter
-=-=-=-=-=-=-=-=-=-=-=
Yes, I'm interested, but I'll have to look at the Proceedings to see
whether I would want to make a presentation.
                ---------------
Date:  7 Jan 1981 1826-PST
From: Neumann
Subject: VERkshop II
To:   VERKshop:

Steve Walker appears to have some good news for the verification and
security communities, and is very eager to convene a VERkshop II.  He
has asked me to round up the usual suspects.  He would like us to meet
in Washington in mid-April (a location that would be of great help to
the government people and less help to the west-coasters among us --
unless you might be returning from April in Paris at the INRIA
Distributed Systems meeting).  If there is a great clamor against DC,
the west coast would be OK.  (I suspect a DC meeting would cut into
the nongovernmental attendance, while a west-coast meeting would lop
off many government people.  Meeting in Texas or Chicago or Omaha
would probably lop off most of both.)  How about a one- to two-day
meeting of the verification-oriented people followed by a one- to
two-day meeting of the security-oriented people, maybe three or four
days in all?  This note is a questionnaire to solicit your answers to
the following questions.

1. ARE YOU INTERESTED IN ATTENDING THE MEETING IN DC?
2. WOULD YOU ATTEND THE MEETING IF IT WERE IN THE LA OR SF AREA?
3. WHICH OF THE FOLLOWING ARE POSSIBLE FOR YOU?
   (3A) 13-15 April?
   (3B) 15-17 April?
   (3C) 20-22 April?
   (3D) 22-24 April?

A fast reply would be appreciated.  The hoped-for response is
something like "YES,YES,ACB", where the acceptable dates are listed
in priority order.

Please add any suggestions, outspoken opinions, desires, etc.  For
your info, the mailing list is appended.  Let me know if you think
there are any glaring omissions.  I hope we can avoid last year's
unfortunate conflict with the protocol community.

Happy New Year!

Peter

-=-=-=-=-=-=-=-=-=-=-=
THIS MAILING WENT TO THE FOLLOWING:
VERKshop:
Adrion@NBS-10,
Ames@ISI,
Cerf@ISI,
Cohen@BBN-TENEXB,
MCorasick@BBN-TENEX, 
Cullyer,
Darr@RADC-TOPS20, 
DEdwards@ISI,
Druffel@isi,
Faust@RADC-Multics,
Fisher@isi,
Denicoff@ISI,
Heafner@NBS-10,
NSF-CS@ISI,
Keeton@ISI,
Lubbes@isi,
Marmor@ISIA, 
Millen@RADC-MULTICS,
NRL@ISI,
BPrice@ISI,
Shotting,
JTaylor@ISI,
Tinto@BBN,
Walker@ISI,     
Wilson@RADC-Multics,
Balzer@ISIE,
Bledsoe@Utexas,
Bochmann,
Boebert@MIT-Multics,
Bonyun@UCLA-S, 
Boyer,
Cohen@UTexas,
Crocker@isie,
Elspas,
Feiertag, 
Flon@ISIC,
Gaines@RAND-UNIX,  
Gerhart@ISIC,
Goguen,
Good@UTexas, 
CCG@SAIL,
DHare,
GHaynes@bbn-TENEXA,
Dick@UCLA-S,     
Lamport,
Levitt,
London@ISIC,
Luckham@SU-AI,       
Manna@SAIL,
Melliar-Smith,
Moore,
Moriconi,
Musser@isic,
Neumann,
Oppen@SU-AI,
Owicki@SU-SCORE,
Polak@SU-AI,
Popek@UCLA-SECURITY,
Pratt@MIT-AI,
LRobinson,
Schwartz,
SDIM,
SDIN,
Sunshine@ISIE,
DThompson@ISIC,
vonHenke@SU-AI,
Bruce@UCLA-S,
Weissman@isia

-------
                ---------------
-------

∂14-Jan-81  0706	Boyer at SRI-F2 (Bob Boyer) 	Course
Date: 14 Jan 1981 0707-PST
From: Boyer at SRI-F2 (Bob Boyer)
Subject: Course
To:   JMC at SU-AI

I'm really pleased at your suggestion about a course at
Stanford, but right now neither J nor I has the time or
inclination to work up a course.

However, I definitely look forward to giving a lecture in
your LISP course next Fall.  It's possible that by then J
and I will have converted our theorem-prover from Interlisp
to Maclisp, so some of the students could even try it out.

I'm glad you're coming to the Verkshop.  Woody has also
indicated he will come.
-------

∂15-Jan-81  1147	NEUMANN at SRI-KL 	VERkshop II progress 
Date: 15 Jan 1981 1130-PST
From: NEUMANN at SRI-KL
Subject: VERkshop II progress
To: VERKshop: ;


The most likely dates for VERkshop II appear to be 21-23 April,
Tues-Thurs, probably in the DC area.  Steve is currently negotiating
with NBS to see if we can hold it there.

Firmer plans, specific goals of the VERkshop, topics to be discussed,
desired contributions, etc., will follow shortly to aid in your
planning.  Please continue to send in your suggestions.  You might
begin to think about what position statements you might wish to write. 
I would again like to collect them on-line, and distribute them in
advance.  They could be self-standing or incremental to last year's.
If you wish, they should be suitable for inclusion in the July 1981 
issue of the SIGSOFT Sofware Engineering Notes (SEN).   (You might also
care to submit something even if you cannot attend!)

This scheduling will leave you West Coasters Monday and/or Friday to
travel if you prefer, or otherwise to visit in the East.  Almost all
Westerners indicated willingness (or in some cases even desire) to go
East.  Thus it seemed reasonable to accommodate the government people
who were urging us to hold it in the East this time.  Excellent
government attendance is expected, including Vint Cerf -- who has
taken over verification and security work at ARPA.

Many thanks to those of you who responded to the initial query.  The
response was very strong.  More soon.  Peter

-------

∂16-Feb-81  1324	NEUMANN at SRI-KL 	VERkshop II
Date: 16 Feb 1981 1306-PST
From: NEUMANN at SRI-KL
Subject: VERkshop II
To: VERKshop: ;

MESSAGE FROM STEVE WALKER TO VERkshoppers:

Sorry for the long delay in commenting on the agenda for VERkshop II.
There have been a number of developments in the past few weeks which
will have a significant impact on the verification community, and I
wanted to have things settle down a bit before commenting.

Many of you are familiar with my efforts over the past few years to
establish a capability for the evaluation of the integrity of computer
systems.  On 1 Jan 1981, the Director of NSA was assigned responsibility 
for a Computer Security Evaluation Center for the DoD.  The Center
will be established as a Program Management Office reporting directly
to the Director and independent of other organizations at NSA.  It
will be separately funded with both an R&D and an industry evaluation
role.  Details of the staffing and organization of the Center are now
being worked out.  I hope more definitive information will be
available by the time the Verkshop is held.

So what does all this mean to the verification community?  One major
impact is that in order to be successful in the long term, the Center
is highly dependent upon the widespread availability of verification
tools and techniques.  Previous R&D in this field was done for the
general benefit of software development.  Now an organization exists
(or soon will) which has a clear charter and a vital interest in the
development of verification techniques.  A second major impact which
will follow from the first is a strong interest in formal specification 
and verification techniques by the computer manufacturing and system
development communities.  This interest will offer significant new
opportunities for technical advances but will also require careful
planning and coordination to avoid chaos.  It is my hope that the
Verkshop attendees can be instrumental in organizing an orderly
approach to this situation.

So what should we do at the Verkshop to begin this process?  I have a
list of agenda items of my own, and I encourage you to suggest others
that you feel are important.  I'm going to ask Bill Wilson of Mitre to
assemble the suggestions and come up with a rough-cut agenda for the
Verkshop.  We shouldn't feel constrainded by a formal agenda but we
need a guideline to be sure we cover what is important.

First to get (re)acquainted and come up to speed, we should have
(very) brief status reports on the major activities of the past
year.  I would like to discuss the Evaluation Center as part of
this time and get your reactions and concerns about the Center.
Then I propose we have a roundtable discussion of the best way(s)
to capitalize on the opportunities for advancing the state of the
art in verification technology being offered by the Center and
the increased industry interest in verification.  What steps
should we take in the next year, five years and ten years?  How
can we develop an effective transfer of technology to the
manufacturers and system developers?  And perhaps most important,
how can we accomplish all this and protect the essential
research nature of the verification community?

Included among the topics of this discussion should be the status of
Ada and the possibilities of developing effective verification
capabilites focused on Ada.  I suggest Ada here because of the
significant efforts underway by many manufacturers to develop Ada
facilities.  If a verification capability can be developed around Ada,
then many of the problems of technology transfer and proliferation of
different techniques can be eased.  However, if Ada is not a suitable
environment for verification systems, then we should realize this
early and begin developing alternative approaches.  Many of you have
participated in the development of Ada or have studied its suitability
for verification.  I hope we can have a good discussion of this area
during the Verkshop.

Protocol verification is an area which must be considered during
our meeting.  I will leave it to others to suggest the best way
to approach this topic.  Marti Branstad and others at NBS are
exploring less formal methods of verification and validation.  I
hope we can spend some time discussing these efforts and how they
complement formal procedures both in the short and long term.

There is a major concern which is emphasized by the establishment
of the Evaluation Center.  Some people have made the argument
that if verification techniques are used to somehow prove the
integrity of a system, then those same techniques could also be
used by an adversary to detect flaws in the system.  This line of
reasoning quickly carries one to the conclusion that any
verification system used on a system which will protect
classified information must itself be protected by being
classified.  I personally believe that while there is a concern
here, the negative impact of general application of this approach
would be so great as to undermine all progress in this field.  We
must come up with reasonable ways to deal with this concern short
of resorting to such self-defeating means as broad scale
classification.  I hope we can spend some time at the Verkshop
discussing this problem and can suggest some potential solutions.

I've probably rambled on enough.  I firmly believe that verification
systems are going to play a major role in the future development of
major computer systems and that we have a good opportunity to
influence that role through meetings like the Verkshop.  I encourage
each of you to prepare your thoughts on the areas I have mentioned and
any others you feel are important, and come prepared to work hard.

Send your agenda items and position papers if you wish to write any to
Peter and Bill Wilson.  The meeting will be April 21-23 at NBS in
Gaithersburg, Md.  More details on location and hotel reservations, etc.,
in a little while.

Steve

-=-=-=-=-=-=-=-=-=-=-=-=-=--=-=-=-=-=-=-=-=-=-=-=-=-=-=
NOTE NET ADDRESSES FOR THOSE OF YOU WITH NET ACCESS:
      Walker@ISI
      Wilson@RADC-Multics
      Neumann@SRI-KL (or in a pinch when KL down, SRI-CSL)
-=-=-=-=-=-=-=-=-=-=-=-=-=--=-=-=-=-=-=-=-=-=-=-=-=-=-=

NOTE FROM PETER NEUMANN:

Please begin to formulate your contributions.  I will distribute all
Verkshop statements received on-line by me prior to 16 April to those
of you with net access, and would hope to be able to hand out in
hard-copy everything received by the 16th on the 21st.  The variety of
formats of last year is probably still appropriate, although if you
stick with basics it will help me.  (See the July 80 ACM SIGSOFT
Software Engineering Notes [SEN], and the contributions that show
particularly clear evidence of my editing.  Please avoid bold face,
underlines, and italics for the NET version, although you may send me
SCRIBE input for hard-copy and publication versions.)  You should also
bring auxiliary material such as reports and relevant published papers
to hand out.

Peter

-------

∂07-Mar-81  2122	NEUMANN at SRI-KL 	[dkb at nbs-unix: Motels near NBS]  
Date:  7 Mar 1981 2057-PST
From: NEUMANN at SRI-KL
Subject: [dkb at nbs-unix: Motels near NBS]
To: VERKshop: ;

Mail-from: ARPAnet host NBS-UNIX rcvd at 6-Mar-81 1214-PST
Date:  6 Mar 1981 at 1513-EST
From: dkb at nbs-unix
Subject: Motels near NBS
To: neumann@sri-kl
 
-----
As per Steve Walker's request, the following list of Motels are
suggested for your meeting in April.  As they fill up often, urge
the participants to get resrvations early.
 
Ramada Inn; 2 exits south of NBS on Rt. 270; 30l-424-4940.
 
Holiday Inn; NBS exit on Rt. 270 and 1 mile East; 301-948-8900.
 
Washingtonian; 1 exit south of NBS on Rt. 270; 301-948-2200.
 
Potomac Sheraton; 1 exit south of NBS on Rt. 270; 301-840-0200.
 
The rates all run close to $50 per night plus 10% tax.  The Washingtonian
is somewhat older and cheaper.
-----
 
                ---------------
-------

∂17-Mar-81  1013	NEUMANN at SRI-KL 	VERkshop II
Date: 17 Mar 1981 0959-PST
From: NEUMANN at SRI-KL
Subject: VERkshop II
To: VERKshop: ;

OK, gang, the time is drawing near to 21-23 April.  I hope you are all
seriously engaged in writing up your contributions.  I imagine that
the agenda would be somewhat driven by what you submit or bring along,
although oral contributions are of course also appropriate.
Nevertheless, we would like to have some sort of advanced warning as
to what you might like to discuss, in an effort to make the VERkshop
as useful to you as possible.

Bill Wilson has supposedly been collecting your suggestions, although
(1) he has received very little from you, (2) his net connection has
been down much of the time, and (3) we didn't push you very hard.  (I
was away for most of the last three weeks.)  So please give us an
early idea of whether you plan on attending, what you might expect to
contribute on-line, and even some idea of topics you might wish to
have discussed orally -- if you can think that far ahead.

[Note: Some of you are receiving this although you have already
indicated you would probably not be able to attend.  You may happily
ignore our requests, although your comments are of course also
welcome.  However, I would appreciate your letting me hear from you,
even if to say that you definitely cannot come, or that you do not
wish to receive the increasingly heavy flurry of mail that can be
expected in the next five weeks.  If you cannot come, the default will
be to send you the final preVERkshop distribution of contributions by
by US Dogsledmail, plus any summary material that we might subsequently 
produce for the SIGSOFT SoftwareEngineeringNotes.]

Several possible broad agenda items currently contemplated include the 
following.

  Presentation and discussion of the CSEC charter (Computer
    Security Evaluation Center).
  Summary progress reports of the last twelve months.
  Practical results and user experience with verification systems.
  Implementation experience in verification systems.
  Policy issues concerning the current state of the art and the future
    of verification.  What are the visible successes?  Are they adequately 
    represented in the literature?  Are the [to-be-distributed] VERkshop II
    contributions reflective of the progress?  Is there an urgent need 
    for more solid demonstrations of the practical applicability in the 
    near future?  Is there expected to be adequate funding?  Is 
    verification oversold?  undersold?  Have DeLiptIs had any 
    real impact?  If that impact is negative, is there any need for a 
    rebuttal to that impact (other than the implicit rebuttal of some 
    dramatic success stories)?

To keep things simple, please address all responses to Neumann@SRI-KL.
You might CC: Wilson@RADC-Multics (if you can get through!) on 
suggested agenda items, although I can forward to him if you forget.
I will keep Steve informed.

A note to West Coasters: remember TWA's new fare, announced yesterday,
effective 20 April: $298.

[A side note, FYI:  As of today, the AI people at SRI are now @SRI-AI
(but residually still also @SRI-KL for a while).  The CSL people are
either @SRI-KL or @SRI-CSL (one of our Foonlys, formerly @SRI-F2).
But mail to SRI-KL will be forwarded as necessary in any case.]

See you soon?  Peter

-------

∂21-Mar-81  0030	Robert S. Boyer <BOYER at SRI-CSL> 	Verkshop 
Date: 21 March 1981  00:30-PST (Saturday)
From: Robert S. Boyer <BOYER at SRI-CSL>
To:   JMC at SU-AI
cc:   Bledsoe at UTexas, Boyer at SRI-CSL
Subject: Verkshop

Are you still thinking of going to the Verkshop?  It may be
a definitive political meeting, though I'm less optimistic
about the technical aspects.

One issue is how NSA should pursue its Computer Security
Evaluation Center charter.  As I understand it, NSA is
setting up a semi-public facility for evaluatiing computer
systems.  It might dictate an interest in proving facts
about computer programs.

I hope that you and Woody Bledsoe show up.

Yes, I still plan to attend.
∂24-Mar-81  0916	NEUMANN at SRI-KL 	VERkshop agenda, first cut
Date: 24 Mar 1981 0843-PST
From: NEUMANN at SRI-KL
Subject: VERkshop agenda, first cut
To: VERKshop: ;

Well, Now that the SRI-KL is up again (yesterday there was no power in
the new building!), I see that I have had only a few responses.
(Note: our Foonly is much more reliable than the KL, so try me at SRI-CSL
[a.k.a. SRI-F2] if the KL won't respond.)  But Steve, Don Good, and I
have been exchanging net notes.  Here then is a summary of current
thinking for your comments.  

Don Good has reiterated the primary goal, namely, to address the issue
of how to attain "widespread availability of of verification tools and
techniques."  We should cover

  1. Where are we now? 

  2. Where do we need go?

  3. How do we get there?

Your contributions (oral or written) should address whichever of these
topics you see fit.  Those of us who have discussed it seem to be in
general agreement that the vital issues at this time are Items 2 and
3, and it is hoped that those vital issues will be the primary focus
of this VERkshop -- following a brief summary of progress.

Following introductory status reports, Don suggests that we turn to
the security community and address the issues of what do they think is
needed, what do they really need, what can the verification community
reasonably provide, what can't it provide, what are reasonable goals
for the future, and how do we attain them.  The main question there is
how can we provide effective verification support for building
verified, secure systems.  On the other hand, I think that Boyer and
Moore feel that the near-term successes are going to come not from
secure systems verification, but from verification of small but VERY
REAL programs [in their case, currently Fortran is receiving their
attention!].  I think it is clear that we should work in both
directions.  We need all the help we can get!

FROM DON GOOD:
If several major discussion issues can be identified, I think
it also would be a good idea to solicit some discussion organizers
in advance to concentrate on rounding up the people who have 
something to say on that issue.  Discussions are usually productive
in direct proportion to the amount of thought people have put into
the topic in advance.  If people want to support these discussions
with written position papers, so much the better.

FROM STEVE WALKER:
Topics I feel we should include in an agenda are:

Status reports from the major verification efforts - SRI,
UTexas,ISI,Stanford, IPSharp ...

Status of DoD verif research support - Walker - Darr, Lubbes,
Marmor-Squires

Status of Computer Security Initiative - Walker - Computer
Security Evaluation Center

General discussion

- where are we now?  - where do we want to be?  - where can we
hope to get?  - what will it take to get there?

Also to be included:

Ada - what role can/should it play (what about Euclid, Gypsy,
etc)

and Protocol Verification - where do we stand


FROM DON GOOD:
Let me propose the following top-level design of an agenda:

Tuesday, April 21.  Status Reports 

  I think it would be good if we could get these all in on the first
  day.  It would discourage lengthy advertising campaigns, and it also
  would give people one extra evening of barroom discussion with all
  of the past years progress reports out in the open.  If there really
  isn't enough time, there would be no major problem with carrying
  over to Wednesday.

Wednesday, April 21.  Assessment of Outstanding Problems.

  The paper I have been preparing has been directed specifically at this
  question.  The outline I have so far is below.  For purposes of general
  discussion, I would think the focus should be on obtaining a community
  assessment of these problems (and whatever other ones folks might think
  are important), and on discussing what degree of solution we need in
  order to make verification  practical.  I would be happy to organize
  a day's worth (or whatever amount is appropriate) around these issues.
  My draft presently is really drafty, but if any of you would like to
  see it, I would be happy to circulate it around.

  1. Verification Issues
     My theme here is that verification currently is impractical
     because it is just too expensive.  We need drastic cost reductions
     to be effective.

     1.1 Transforming Specified Programs into Theorems
         This provides a forum for discussing proof methods for
	 protocols, concurrency, exception handling, generics, ....
	 and other outstanding verification problems and techniques.

     1.2 Languages.
	 This provides the forum for discussion of both programming
	 languages and specification languages.  The ADA issue is
	 one of the important ones that needs to be discussed.

     1.3 Verification Systems.
	 Here we need to discuss what state our systems are in
	 presently, how for we can reasonably expect them to
	 be pushed, what should future systems look like....?
         I would include theorem provers as a part of this discussion.

     1.4 Absence of High Level Theories.
         (Or as Sue Gerhart calls it, the "knowledge gap.").  I think
	 the issues here whether other people think this is as serious 
	 a problem as Sue and I do, and if so, what we can reasonably
         expect to attain in this area.

  2. Security Issues.
     My focal issue here is that if we really want to build verified,
     secure systems, the verification community and the security 
     community have to join forces.  We have to USE verification
     throughout the entire system building process.  We need to move
     past building secure systems with verification "in mind", and
     we need to seriously consider alternatives to security kernels
     which are essentially verification retrofit efforts.  From near
     the beginning, we verification folks have said that retrofitting
     won't work.
     
Thursday, April 23.  How to Solve Them.

  This is the really difficult question, and I put it here just to be
  sure there would be some time for discussion before people begin
  catching planes.  I think we definitely need to get started on it
  first thing Thursday am.

  I really don't have any specific answers to propose here.  It clearly
  would be better if someone had some specific proposal to serve as
  a focal point for a discussion.  Maybe the Government has some plans
  to lay on the table for discussion.

FROM PETER:  SO, PLEASE LET US HAVE YOUR COMMENTS.  RESPONSES TO ME
@SRI-KL (or @SRI-CSL if KL down).  I WILL REDISTRIBUTE AS APPROPRIATE.  
I ALSO NEED TO KNOW FAIRLY SOON FROM EACH OF YOU WHO WOULD LIKE TO
COME.  WE MAY HAVE TO HAVE A CUTOFF ON ATTENDANCE IF MORE PEOPLE WOULD
LIKE TO COME THAN THE FACILITIES WILL HOLD.  (HOWEVER, I HOPE THAT
WILL NOT BE NECESSARY.)

-------

∂30-Mar-81  1216	NEUMANN at SRI-KL 	VERkshop II: Formal Application for Participation Needed!    
Date: 30 Mar 1981 1200-PST
From: NEUMANN at SRI-KL
Subject: VERkshop II: Formal Application for Participation Needed!
To: VERKshop: ;

Subject: VERkshop II

If everyone who has indicated he might come or would like to come were
actually to come to VERkshop II, we would have something more like 90
people instead of the 50 that we should really have if we are to have
any meaningful discussion.  On the other hand, we haven't heard from
most of you as to whether you really are planning on coming.  Thus,
please respond quickly, even if your answer is NO, and we will try to
turn it around and decide who actually can come among the various
requestees.  (Perhaps there will be enough NOs that we won't even have
to turn people away.)  A quick reply will do.

For those of you who have replied in the last week, or who consider
yourself on this list for information purposes only, you may ignore
this message.  Thanks.  Peter

-------
I will definitely come to the Verkshop.
∂06-Apr-81  1451	NEUMANN at SRI-KL 	[DUCKETT at USC-ISIE: Verkshop II/IPTO Contribution]    
Date:  6 Apr 1981 1429-PST
From: NEUMANN at SRI-KL
Subject: [DUCKETT at USC-ISIE: Verkshop II/IPTO Contribution]
To: VERKshop: ;

OK, gang, despite Vint's presumably still being worried about his
income tax return, he was this year again able to come in early in
filing his VERkshop return.  I am redistributing it at this time to
help jog you all into action, if you haven't yet thought about what
you might want to send in for redistribution.  The deadline for
getting your thoughts into the main handouts to be distributed is
probably Wednesday AM, 15 April.  You may subsequently revise your
contributions if you wish them to appear in SEN -- the deadline for
that is 21 June.  Peter
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

                    A View of Verification Technology
                            Vinton G. Cerf
                              DARPA/IPTO
                            2 April 1981
INTRODUCTION:
Verification technology has been the subject of research for a number of
years, now, supported by a variety of agencies for a variety of reasons.
Research problems have ranged from specification language design to the 
implementation of automatic theorem provers.  The simple premise of this
brief note is that further progress is possible, but that it should be 
guided by deliberate application of the technology to a series of 
incresingly demanding and real problems.  Artificial problems should be 
used only if they are needed to test some aspect of a new system or 
techniques.

If a parallel with compiler technology may be drawn, serious progress 
was only made in efficient compilation when users became dependent on 
compilers for serious, production work.

PRACTICAL APPLICATIONS:
IPTO is supporting the use of AFFIRM for specifying and proving theorems
about communication protocol behavior.  These theorems geneally have to 
do with functionality, consistency, progress and the like.  Debugging of
protocol specifications has been aided by this effort.  For example, 
USC-ISI identified a bug in the TCP specification document by this 
means.

The State Delta system at ISI is being applied to microcode protocol 
and, eventually distributed algorithm verification.  Each new feature 
planned during the state delta development is driven by the needs of 
each new, increasingly demanding application.  An important area of 
interest is the ability to provide proofs of the correctness of 
microcodes used to enforce certain aspects of computer or system 
security.

RECOMMENDATIONS:
The verification community should review the applications now driving 
their development and research - some common applications should be 
attempted to permit comparisons among the various verification systems. 
The AB protocol has been a popular candidate, but more elaborate 
problems are needed.

A fundamental issue has to do with the ability of verification systems 
to scale - that is, to accommodate larger programs/protocols without 
exhibiting uncontrolled growth in processing time and/or storage 
requirements.  We need to understand which of the various existing or 
evolving systems are organized for production work.
Furthermore, the problem of integration of PV systems into normal 
programming support environments must be addressed.  How does a PV 
system map into the traditional edit/compile/debug/document paradigm of 
software development?
-------

∂09-Apr-81  1217	NEUMANN at SRI-KL 	Agenda.  Respond if desired.   
Date:  9 Apr 1981 1201-PST
From: NEUMANN at SRI-KL
Subject: Agenda.  Respond if desired.
To: VERKshop: ;


VERkshop II, NBS, 21-23 April 1981, Logistic Instructions to follow.

Following is the Tentative VERkshop II Agenda.
READ IT NOW.  YOUR RESPONSE IS NEEDED QUICKLY.  SEE ITEMS AT END.

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
The first day will be devoted to very brief summary reports of present
work.  The second and third days will concentrate on the questions of
where are we now, where we should be going, and how we can best get
there, for each of the suggested topics. (Session coordinators are
indicated in parentheses.)
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-

Tuesday, April 21.  BRIEF Status Reports (Neumann) ******[Note 1]******

9:00-12:30 Government Reports
              (C3I, NSA, Air Force, Navelex, NRL, ...)
           Other Reports 
              (SRI, Stanford, ISI, Texas, SDC, I.P.Sharp, Digicomp, ...)

12:30-13:30 Lunch

13:30-17:30 Research Reports Continued

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-

Wednesday, April 21.  Future Security and Verification Issues

 9:00- 9:15  Intended focus of remaining discussion (Good)
 9:15-10:15  Security Issues -- Kernels (Popek)
10:15-10:30  Break
10:30-11:30  Security Issues -- Others (Neumann)

11:30-12:30  Lunch

12:30-13:30  Proving properties about specifications (Wilson)
13:30-14:30  Proving properties about specified programs (von Henke)
14:30-14:45  Break
14:45-15:45  Protocols (Cerf)
15:45-17:00  Programming and Specification Languages (Bonyun)

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-

Thursday April 23.  Future Verification Issues, Continued

 9:00-10:15  Verification Systems (Good)
10:15-10:30  Break
10:30-11:30  Theorem Provers and Checkers (Moore)
11:30-12:30  High-Level Theories (Gerhart)

12:30-13:30  Lunch

13:30-14:30  Prototype Applications to Drive Future Research (Crocker)
                                                  ******[Note 2]******
14:30-15:30  Space for other topics                
15:30-16:30  Summary/Wrap-up
-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-

******[Note 1]****** PLEASE NOTIFY NEUMANN@SRI-KL IF YOU WOULD LIKE A
PIECE OF TIME ON TUESDAY, AND HOW MUCH (min to max).  PLAN ON GIVING
ONLY BRIEF SUMMARIES, AND HAND OUT THE DETAILS.

******[Note 2]****** PLEASE LET STEVE CROCKER KNOW (NETMAIL to
Crocker@ISIF, cc NEUMANN@SRI-KL) OF YOUR SUGGESTIONS FOR SIGNIFICANT
FUTURE PROTOTYPE APPLICATIONS THAT MIGHT VALUABLY DRIVE AND SUPPORT
VERIFICATION RESEARCH IN THE FUTURE.  Please flood us with ideas, even
if you will not be attending.  We have asked Steve to collect and
organize these ideas.  He will not be in LA during the penultimate
week (13 April), but will read his mail.

Thanks.  Peter
-------

∂16-Apr-81  0405	NEUMANN at SRI-KL 	VERkshop: ON-LINE COPY-- DEFAULT NO!
Date: 16 Apr 1981 0400-PST
From: NEUMANN at SRI-KL
Subject: VERkshop: ON-LINE COPY-- DEFAULT NO!
To: VERKshop: ;

OK, gang, we are still waiting for the info from NBS on which BLDG and
ROOM.  We would really like to start at 9AM sharp on Tuesday, and it
is apparently not in the main building....  so plan accordingly.

I now have contributions from Cerf, Texas (2), ISI (3), SDC (1 plus
a statement from Clark Weissman on driving applications), SRI,
Ford, Sytek, Mitre (2), and TI.  I expect more from SRI, SAIL, etc.

The volume is again large, athough not yet as profuse as last year.
In the interest of not overloading the NET, my directory (which is
running 800-900 pages most of the time these days), and my sanity in
dealing with directory overflows, I would like to make the default NO
NET COPY unless you explicitly ask for one today or tomorrow.  If you
do ask, I will be happy to send you what is available, probably late
Thursday.  Try to get together and only ask for one per location.  You
should get a hard-copy on Tuesday in any event, if all goes well.

Peter
-------

∂16-Apr-81  1407	NEUMANN at SRI-KL 	How to get there.    
Date: 16 Apr 1981 1354-PST
From: NEUMANN at SRI-KL
Subject: How to get there.
To: VERKshop: ;

⊗
FROM STEVE WALKER:

As you enter the NBS Main Gate (Visitors Entrance), turn left on North
Drive.  Proceed toward (9-story) the Main Building.  Turn left on
East Drive toward Visitors Parking area (a right turn here would take
you to the Technology Building).  Proceed on East Drive, past Visitors
Parking area and the next parking area.  Park in the third parking
area and proceed to Building 220 Metrology Building.  The conference
will be held in Room A62 which is in the A corridor on the ground (or
basement) level.

GOOD LUCK!  SEE YOU THERE.
-------

∂16-Apr-81  2211	NEUMANN at SRI-KL 	[dkb at nbs-unix: Third try at sending Meeting Directions]   
Date: 16 Apr 1981 2204-PST
From: NEUMANN at SRI-KL
Subject: [dkb at nbs-unix: Third try at sending Meeting Directions]
To: VERKshop: ;

ON THE GROUNDS THAT REDUNDANCY MAY BE VALUABLE, AND SINCE DENNY WENT
TO THE TROUBLE OF GENERATING THIS MESSAGE, I THOUGHT I MIGHT AS WELL
FORWARD THIS ONE TO YOU ALL!!!  P.
                ---------------
From: dkb at nbs-unix

As per the request of Steve Walker, I offer the following directions
to get to the Software Verification Meeting at NBS on April 21-23.
Room A-62 of the Metrology Building (Number 220) is reserved for the
meeting.  Come to NBS via Rt. 270 and via Quince Orchard Rd.  The
exit from Rt. 270 is about 10 miles northwest of the Washington
Beltway (Rt. 495) towards Frederick.  The NBS exit is marked.
Go straight ahead at the first two stop lights (there's a new one)
and make a left onto the NBS campus.  Go straight ahead for about 1/2
mile and make a left in front of the Technology Building.  This curves
right and goes in front on the 11 story administration building.  Go
two buildings past the administration building and park in the lot
in front of the second building.  This should be Metrology.
Go into the basement, A corridor, room A62.  Coffee and donuts will
be waiting.  Good luck on finding us.  If necessary, call Dennis
Branstad on (301)921-3861 or ask for TINA on this number.
-------